Terminal identifiers

It is possible to use identifiers as terminals, with optional user-specified formatting. To declare identifiers as terminals, use To declare an identifier as a terminal with user-specified formatting, use Henceforth, text will be used to format the terminal named identifier. For example, the following commands can be used to use special TEX characters as nonterminals: